Problem:
 active(incr(nil())) -> mark(nil())
 active(incr(cons(X,L))) -> mark(cons(s(X),incr(L)))
 active(adx(nil())) -> mark(nil())
 active(adx(cons(X,L))) -> mark(incr(cons(X,adx(L))))
 active(nats()) -> mark(adx(zeros()))
 active(zeros()) -> mark(cons(0(),zeros()))
 active(head(cons(X,L))) -> mark(X)
 active(tail(cons(X,L))) -> mark(L)
 active(incr(X)) -> incr(active(X))
 active(cons(X1,X2)) -> cons(active(X1),X2)
 active(s(X)) -> s(active(X))
 active(adx(X)) -> adx(active(X))
 active(head(X)) -> head(active(X))
 active(tail(X)) -> tail(active(X))
 incr(mark(X)) -> mark(incr(X))
 cons(mark(X1),X2) -> mark(cons(X1,X2))
 s(mark(X)) -> mark(s(X))
 adx(mark(X)) -> mark(adx(X))
 head(mark(X)) -> mark(head(X))
 tail(mark(X)) -> mark(tail(X))
 proper(incr(X)) -> incr(proper(X))
 proper(nil()) -> ok(nil())
 proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
 proper(s(X)) -> s(proper(X))
 proper(adx(X)) -> adx(proper(X))
 proper(nats()) -> ok(nats())
 proper(zeros()) -> ok(zeros())
 proper(0()) -> ok(0())
 proper(head(X)) -> head(proper(X))
 proper(tail(X)) -> tail(proper(X))
 incr(ok(X)) -> ok(incr(X))
 cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
 s(ok(X)) -> ok(s(X))
 adx(ok(X)) -> ok(adx(X))
 head(ok(X)) -> ok(head(X))
 tail(ok(X)) -> ok(tail(X))
 top(mark(X)) -> top(proper(X))
 top(ok(X)) -> top(active(X))

Proof:
 Bounds Processor:
  bound: 10
  enrichment: match
  automaton:
   final states: {15,14,13,12,11,10,9,8,7}
   transitions:
    zeros3() -> 58*
    ok4(67) -> 51*
    ok4(79) -> 87*
    ok4(78) -> 86*
    adx4(69) -> 77*
    adx4(64) -> 51*
    adx4(58) -> 67*
    cons4(87,86) -> 74*
    cons4(79,78) -> 80*
    cons4(61,58) -> 67*
    cons4(63,42) -> 51*
    active4(67) -> 70*
    active4(42) -> 64*
    active4(44) -> 63*
    top4(70) -> 15*
    mark3(69) -> 64*
    mark4(80) -> 74*
    mark4(77) -> 51*
    adx5(80) -> 84*
    adx5(74) -> 70*
    active5(105) -> 91*
    active5(61) -> 73*
    active5(58) -> 74*
    cons5(97,96) -> 92*
    cons5(79,78) -> 98*
    cons5(73,58) -> 70*
    proper4(77) -> 70*
    proper4(61) -> 87*
    proper4(58) -> 86*
    04() -> 79*
    zeros4() -> 78*
    proper5(84) -> 91*
    proper5(79) -> 97*
    proper5(69) -> 74*
    proper5(78) -> 96*
    mark5(84) -> 70*
    active0(5) -> 7*
    active0(2) -> 7*
    active0(4) -> 7*
    active0(6) -> 7*
    active0(1) -> 7*
    active0(3) -> 7*
    top5(91) -> 15*
    incr0(5) -> 8*
    incr0(2) -> 8*
    incr0(4) -> 8*
    incr0(6) -> 8*
    incr0(1) -> 8*
    incr0(3) -> 8*
    adx6(92) -> 91*
    adx6(101) -> 151*
    adx6(98) -> 105*
    adx6(78) -> 108*
    nil0() -> 1*
    proper6(110) -> 118*
    proper6(80) -> 92*
    mark0(5) -> 2*
    mark0(2) -> 2*
    mark0(4) -> 2*
    mark0(6) -> 2*
    mark0(1) -> 2*
    mark0(3) -> 2*
    ok5(102) -> 133,97
    ok5(101) -> 141,96
    ok5(98) -> 74*
    cons0(3,1) -> 9*
    cons0(3,3) -> 9*
    cons0(3,5) -> 9*
    cons0(4,2) -> 9*
    cons0(4,4) -> 9*
    cons0(4,6) -> 9*
    cons0(5,1) -> 9*
    cons0(5,3) -> 9*
    cons0(5,5) -> 9*
    cons0(6,2) -> 9*
    cons0(1,2) -> 9*
    cons0(6,4) -> 9*
    cons0(1,4) -> 9*
    cons0(6,6) -> 9*
    cons0(1,6) -> 9*
    cons0(2,1) -> 9*
    cons0(2,3) -> 9*
    cons0(2,5) -> 9*
    cons0(3,2) -> 9*
    cons0(3,4) -> 9*
    cons0(3,6) -> 9*
    cons0(4,1) -> 9*
    cons0(4,3) -> 9*
    cons0(4,5) -> 9*
    cons0(5,2) -> 9*
    cons0(5,4) -> 9*
    cons0(5,6) -> 9*
    cons0(6,1) -> 9*
    cons0(1,1) -> 9*
    cons0(6,3) -> 9*
    cons0(1,3) -> 9*
    cons0(6,5) -> 9*
    cons0(1,5) -> 9*
    cons0(2,2) -> 9*
    cons0(2,4) -> 9*
    cons0(2,6) -> 9*
    ok6(105) -> 70*
    ok6(152) -> 194,147
    ok6(151) -> 132*
    ok6(106) -> 92*
    ok6(148) -> 145*
    ok6(155) -> 128*
    s0(5) -> 10*
    s0(2) -> 10*
    s0(4) -> 10*
    s0(6) -> 10*
    s0(1) -> 10*
    s0(3) -> 10*
    05() -> 102*
    adx0(5) -> 11*
    adx0(2) -> 11*
    adx0(4) -> 11*
    adx0(6) -> 11*
    adx0(1) -> 11*
    adx0(3) -> 11*
    zeros5() -> 101*
    nats0() -> 3*
    cons6(117,78) -> 92*
    cons6(102,151) -> 155*
    cons6(79,108) -> 109*
    cons6(102,101) -> 106*
    zeros0() -> 4*
    ok7(197) -> 181*
    ok7(204) -> 201*
    ok7(159) -> 186,144
    ok7(114) -> 91*
    ok7(206) -> 203*
    ok7(156) -> 118*
    ok7(160) -> 138*
    00() -> 5*
    adx7(152) -> 159*
    adx7(127) -> 118*
    adx7(194) -> 186*
    adx7(141) -> 132*
    adx7(106) -> 114*
    adx7(101) -> 120*
    head0(5) -> 12*
    head0(2) -> 12*
    head0(4) -> 12*
    head0(6) -> 12*
    head0(1) -> 12*
    head0(3) -> 12*
    active6(114) -> 118*
    active6(79) -> 117*
    active6(98) -> 92*
    tail0(5) -> 13*
    tail0(2) -> 13*
    tail0(4) -> 13*
    tail0(6) -> 13*
    tail0(1) -> 13*
    tail0(3) -> 13*
    mark6(110) -> 91*
    proper0(5) -> 14*
    proper0(2) -> 14*
    proper0(4) -> 14*
    proper0(6) -> 14*
    proper0(1) -> 14*
    proper0(3) -> 14*
    incr6(109) -> 110*
    ok0(5) -> 6*
    ok0(2) -> 6*
    ok0(4) -> 6*
    ok0(6) -> 6*
    ok0(1) -> 6*
    ok0(3) -> 6*
    top6(118) -> 15*
    top0(5) -> 15*
    top0(2) -> 15*
    top0(4) -> 15*
    top0(6) -> 15*
    top0(1) -> 15*
    top0(3) -> 15*
    incr7(155) -> 156*
    incr7(151) -> 162*
    incr7(121) -> 122*
    incr7(128) -> 118*
    top1(37) -> 15*
    proper7(122) -> 137*
    proper7(109) -> 128*
    proper7(79) -> 133*
    proper7(101) -> 194*
    proper7(108) -> 132*
    proper7(78) -> 141*
    active1(5) -> 37*
    active1(2) -> 37*
    active1(4) -> 37*
    active1(6) -> 37*
    active1(1) -> 37*
    active1(3) -> 37*
    active7(102) -> 131*
    active7(156) -> 137*
    active7(106) -> 127*
    proper1(5) -> 37*
    proper1(2) -> 37*
    proper1(4) -> 37*
    proper1(6) -> 37*
    proper1(1) -> 37*
    proper1(3) -> 37*
    mark7(122) -> 118*
    mark7(164) -> 137*
    ok1(35) -> 37,14
    ok1(25) -> 25,9
    ok1(20) -> 37,14
    ok1(27) -> 27,10
    ok1(29) -> 29,11
    ok1(31) -> 31,12
    ok1(33) -> 33,13
    ok1(23) -> 23,8
    ok1(18) -> 37,14
    cons7(131,101) -> 127*
    cons7(133,132) -> 128*
    cons7(163,162) -> 164*
    cons7(102,120) -> 121*
    cons7(131,151) -> 138*
    cons7(148,159) -> 160*
    tail1(5) -> 33*
    tail1(2) -> 33*
    tail1(4) -> 33*
    tail1(6) -> 33*
    tail1(1) -> 33*
    tail1(3) -> 33*
    top7(137) -> 15*
    head1(5) -> 31*
    head1(2) -> 31*
    head1(4) -> 31*
    head1(6) -> 31*
    head1(1) -> 31*
    head1(3) -> 31*
    incr8(160) -> 168*
    incr8(159) -> 172*
    incr8(186) -> 180*
    incr8(138) -> 137*
    adx1(5) -> 29*
    adx1(2) -> 29*
    adx1(4) -> 29*
    adx1(6) -> 29*
    adx1(1) -> 29*
    adx1(18) -> 19*
    adx1(3) -> 29*
    proper8(120) -> 144*
    proper8(162) -> 180*
    proper8(152) -> 203*
    proper8(102) -> 145*
    proper8(164) -> 170*
    proper8(151) -> 186*
    proper8(121) -> 138*
    proper8(101) -> 147*
    proper8(163) -> 181*
    s1(5) -> 27*
    s1(2) -> 27*
    s1(4) -> 27*
    s1(6) -> 27*
    s1(1) -> 27*
    s1(3) -> 27*
    cons8(185,159) -> 179*
    cons8(181,180) -> 170*
    cons8(173,172) -> 174*
    cons8(145,144) -> 138*
    cons8(197,172) -> 211*
    cons1(2,6) -> 25*
    cons1(3,1) -> 25*
    cons1(3,3) -> 25*
    cons1(3,5) -> 25*
    cons1(4,2) -> 25*
    cons1(4,4) -> 25*
    cons1(4,6) -> 25*
    cons1(5,1) -> 25*
    cons1(5,3) -> 25*
    cons1(5,5) -> 25*
    cons1(6,2) -> 25*
    cons1(1,2) -> 25*
    cons1(6,4) -> 25*
    cons1(1,4) -> 25*
    cons1(6,6) -> 25*
    cons1(1,6) -> 25*
    cons1(2,1) -> 25*
    cons1(2,3) -> 25*
    cons1(2,5) -> 25*
    cons1(3,2) -> 25*
    cons1(3,4) -> 25*
    cons1(3,6) -> 25*
    cons1(4,1) -> 25*
    cons1(4,3) -> 25*
    cons1(4,5) -> 25*
    cons1(5,2) -> 25*
    cons1(5,4) -> 25*
    cons1(5,6) -> 25*
    cons1(20,18) -> 19*
    cons1(6,1) -> 25*
    cons1(1,1) -> 25*
    cons1(6,3) -> 25*
    cons1(1,3) -> 25*
    cons1(6,5) -> 25*
    cons1(1,5) -> 25*
    cons1(2,2) -> 25*
    cons1(2,4) -> 25*
    06() -> 148*
    incr1(5) -> 23*
    incr1(2) -> 23*
    incr1(4) -> 23*
    incr1(6) -> 23*
    incr1(1) -> 23*
    incr1(3) -> 23*
    adx8(147) -> 144*
    adx8(206) -> 212*
    adx8(203) -> 198*
    01() -> 20*
    zeros6() -> 152*
    zeros1() -> 18*
    ok8(212) -> 198*
    ok8(172) -> 180*
    ok8(211) -> 170*
    ok8(208) -> 193*
    ok8(168) -> 137*
    nats1() -> 35*
    active8(155) -> 138*
    active8(168) -> 170*
    active8(148) -> 185*
    nil1() -> 35*
    s7(102) -> 163*
    s7(148) -> 197*
    mark1(25) -> 25,9
    mark1(27) -> 27,10
    mark1(29) -> 29,11
    mark1(19) -> 37,7
    mark1(31) -> 31,12
    mark1(33) -> 33,13
    mark1(23) -> 23,8
    top8(170) -> 15*
    top2(39) -> 15*
    incr9(212) -> 215*
    incr9(179) -> 170*
    incr9(198) -> 192*
    active2(35) -> 39*
    active2(20) -> 39*
    active2(18) -> 39*
    active9(160) -> 179*
    active9(197) -> 217*
    active9(204) -> 224*
    active9(211) -> 188*
    proper2(20) -> 49*
    proper2(19) -> 39*
    proper2(18) -> 48*
    mark8(174) -> 170*
    adx2(42) -> 43*
    adx2(48) -> 39*
    s8(145) -> 181*
    s8(204) -> 208*
    s8(148) -> 173*
    s8(185) -> 217*
    cons2(44,42) -> 43*
    cons2(49,48) -> 39*
    top9(188) -> 15*
    mark2(43) -> 39*
    proper9(172) -> 192*
    proper9(174) -> 188*
    proper9(159) -> 198*
    proper9(173) -> 193*
    proper9(148) -> 201*
    02() -> 44*
    cons9(208,215) -> 218*
    cons9(193,192) -> 188*
    cons9(217,172) -> 188*
    zeros2() -> 42*
    s9(224) -> 223*
    s9(201) -> 193*
    top3(51) -> 15*
    07() -> 204*
    proper3(42) -> 52*
    proper3(44) -> 53*
    proper3(43) -> 51*
    zeros7() -> 206*
    ok2(42) -> 48*
    ok2(44) -> 49*
    ok9(218) -> 188*
    ok9(215) -> 192*
    ok3(61) -> 53*
    ok3(56) -> 39*
    ok3(58) -> 52*
    top10(220) -> 15*
    adx3(52) -> 51*
    adx3(42) -> 56*
    active10(218) -> 220*
    active10(208) -> 223*
    cons3(44,42) -> 56*
    cons3(61,58) -> 69*
    cons3(53,52) -> 51*
    cons10(223,215) -> 220*
    active3(56) -> 51*
    03() -> 61*
  problem:
   
  Qed